package Main;

import java.io.File;
import java.io.IOException;
import java.io.PrintWriter;

import javax.xml.parsers.ParserConfigurationException;

import org.apache.commons.lang.NotImplementedException;
import org.xml.sax.SAXException;

import ru.ifmo.automata.statemachine.IAction;
import ru.ifmo.automata.statemachine.IAutomataContext;
import ru.ifmo.automata.statemachine.ICondition;
import ru.ifmo.automata.statemachine.IEvent;
import ru.ifmo.automata.statemachine.IState;
import ru.ifmo.automata.statemachine.IStateMachine;
import ru.ifmo.automata.statemachine.IStateTransition;
import ru.ifmo.automata.statemachine.impl.AutomataContext;
import ru.ifmo.automata.statemachine.impl.AutomataFormatException;
import ru.ifmo.automata.statemachine.io.StateMachineReader;
import ru.ifmo.ltl.LtlParseException;
import ru.ifmo.ltl.buchi.IBuchiAutomata;
import ru.ifmo.ltl.buchi.ITranslator;
import ru.ifmo.ltl.buchi.translator.JLtl2baTranslator;
import ru.ifmo.ltl.buchi.translator.Ltl2baTranslator;
import ru.ifmo.ltl.converter.ILtlParser;
import ru.ifmo.ltl.converter.LtlParser;
import ru.ifmo.ltl.grammar.LtlNode;
import ru.ifmo.ltl.grammar.predicate.IPredicateFactory;
import ru.ifmo.ltl.grammar.predicate.annotation.Predicate;
import structures.AutomateBuhi;
import structures.Graph;
import structures.State;

public class MyTestMain{
	protected static LtlParser parser;
	
	protected static void setUp1() throws IOException, AutomataFormatException {
        SimplePredicateFactory predicates = new SimplePredicateFactory();
        //IAutomataContext context = new AutomataContext(new StateMachineReader("CarA1.xml"));
        parser = new LtlParser(predicates);
    }	
	public static void main(String[] args) throws LtlParseException, IOException, AutomataFormatException, ParserConfigurationException, SAXException, InterruptedException
	{
        setUp1();
		String expr = "F (p2())";
        LtlNode node = parser.parse(expr);
        Ltl2baTranslator ltl2ba = new Ltl2baTranslator();
        String automata = translate(ltl2ba, node);
        System.err.println(automata);
        
        AutomateBuhi automate = AutomateBuhi.loadFromFormulaConvertion(automata);
        System.err.println(automate.startState.getStatesArray().length);
        File xml = new File("testall.xstd");
        AutomateBuhi automate2 = new AutomateBuhi(xml);
        System.err.println(automate2.startState.getStatesArray().length);
        
        AutomateBuhi result = automate2.intersectWith(automate);
        Graph graph = Graph.getFromAutomate(result);
        State[] states = result.startState.getStatesArray();
        
        
        System.err.println("bad one:"+graph.containsStrongComponents());
                        
        states = result.startState.getStatesArray();      
        System.err.println("Size = " + states.length);
        int i =5;
        ++i;
        
        
    }

	protected static String translate(Ltl2baTranslator t, LtlNode node) {
        long time = System.currentTimeMillis();
        String s = t.translate(node);
        time = System.currentTimeMillis() - time;
        System.out.println(t.getClass().getName() + " time = " + time);
        return s;
    }

    protected static ITranslator getTranslator() {
        return null;
    }
    protected void setUp() throws IOException, AutomataFormatException {
        SimplePredicateFactory predicates = new SimplePredicateFactory();
        //IAutomataContext context = new AutomataContext(new StateMachineReader("CarA1.xml"));
        parser = new LtlParser(predicates);
    }

    protected IBuchiAutomata extractBuchi(String expr) throws LtlParseException {
        LtlNode t = parser.parse(expr);
        ITranslator translator = getTranslator();
        return translator.translate(t);
    }

    private static class SimplePredicateFactory implements IPredicateFactory<IState> {
        @Predicate
        public boolean p1() {
            return true;
        }

        @Predicate
        public boolean p2() {
            return false;
        }

        @Predicate
        public boolean p3() {
            return true;
        }

        @Predicate
        public boolean p4() {
            return true;
        }

        public void setAutomataState(IState state, IStateTransition transition) {
            throw new NotImplementedException();
        }

        @Predicate
        public Boolean wasEvent(IEvent e) {
            throw new NotImplementedException();
        }

        public Boolean isInState(IStateMachine<? extends IState> a, IState s) {
            throw new NotImplementedException();
        }

        @Predicate
        public Boolean wasInState(IStateMachine<? extends IState> a, IState s) {
            throw new NotImplementedException();
        }

        @Predicate
        public boolean cameToFinalState() {
            throw new NotImplementedException();
        }

        @Predicate
        public Boolean wasAction(IAction z) {
            throw new NotImplementedException();
        }

        @Predicate
        public Boolean wasFirstAction(IAction z) {
            throw new NotImplementedException();
        }

        @Predicate
        public boolean wasTrue(ICondition cond) {
            throw new NotImplementedException();
        }

        @Predicate
        public boolean wasFalse(ICondition cond) {
            throw new NotImplementedException();
        }
    }
}
